1. Field of the Invention
The invention relates to a method to verify preprocessed Java® (Java® is a trademark or registered trademark of Sun Microsystems, Inc. in the United States and other countries) code. Essentially it comprises a conversion step after which language verification of non-preprocessed Java® code is utilized. In particular, a technical solution is suggested that allows for the conversion of preprocessed Java® card converted applet (hereinafter CAP) files back into standard Java® class files. This conversion can be achieved in a provably correct way, thus solving the problem of language verifying Java® card CAP files. The proposed concept is also applicable to preprocessed code in languages other than Java®.
2. Description of the Related Art
Java® is an interpreted language defined independently of any particular hardware environment which features high-level language operations. Therefore, Java® is extremely well suited for use in embedded microcontrollers. However, due to the size constraints in typical embedded systems, neither the full Java® language set, nor the complete execution and loading format as defined for Java® on PCs can be sustained in such embedded microcontroller devices. Therefore, it is a common technique to preprocess or convert the regular, PC-oriented Java® code, also called class files, into a format suitable for loading and execution on embedded microcontrollers. One concrete example where this has been firmly specified is in the area of the Java® card, a chip card featuring a subsetted Java® interpreter.
One goal of executing Java® code is to attain a level of security and trust that can not be achieved by using machine language programs alone. This is due to the interpreted nature of the language and the thus inherent continuous checks of the Java® code prior to its actual execution. One common feature providing this trust is a so-called Java® class verifier run at development time of the Java® code. It checks, for example, static object/class relationships as well as basic scoping rules, i.e., whether a particular method has access to another class's data or code. Programs to perform this work are available.
Java® card technology enables programs written in the Java® programming language to be run on chipcards, smart cards and other small, resource-constrained devices. Developers can build and test programs using standard software development tools and environments, then convert them into a form that can be installed onto a Java® card technology enabled device. Application software for the Java® card platform is called an applet, or more specifically, a Java® card applet or card applet (to distinguish it from browser applets). While Java® card technology enables programs written in the Java® programming language to run on chipcards, such small devices are far too underpowered to support the full functionality of the Java® platform. Therefore, the Java® card platform supports only a carefully chosen, customized subset of the features of the Java® platform. This subset provides features that are well-suited for writing programs for small devices and preserves the object-oriented capabilities of the Java® programming language. The role of the Java® card virtual machine is best understood in the context of the process for production and deployment of Java® card software. There are several components that make up a Java® card system, including the Java® card virtual machine, the Java® card converter, a terminal installation tool, and an installation program that runs on the device.
Development of a Java® card applet begins as with any other Java® program. A developer writes one or more Java® classes, and compiles the source code with a Java® compiler, producing one or more class files. The applet is run, tested and debugged on a workstation using simulation tools to emulate the device environment. Then, when an applet is ready to be downloaded to a device, the class files comprising the applet are converted to a Java® card CAP file, also called converted applet file, using a Java® card converter. The Java® card converter takes as input not only the class files to be converted, but also one or more export files. An export file contains name and link information for the contents of other packages that are imported by the classes being converted. When an applet or library package is converted, the converter can also produce an export file for that package.
After conversion, the Java® card CAP file is copied to a card terminal, such as a desktop computer with a card reader peripheral. Then an installation tool on the terminal loads the Java® card CAP file and transmits it to the Java® card technology enabled device. An installation program on the device receives the contents of the Java® card CAP file and prepares the applet to be run by the Java® card virtual machine. The virtual machine itself need not load or manipulate Java® card CAP files; it need only execute the applet code found in the Java® card CAP file that was loaded onto the device by the installation program. The division of functionality between the Java® card virtual machine and the installation program keeps both the virtual machine and the installation program small. The installation program may be implemented as a Java® program and executed on top of the Java® card virtual machine. Since Java® card instructions are denser than typical machine code, this may reduce the size of the installer. The modularity may enable different installers to be used with a single Java® card virtual machine implementation.
It would be ideal if programs for chipcards could be written using all of the Java® programming language, but a full implementation of the Java® virtual machine is far too large to fit on even the most advanced resource-constrained devices available today. A typical resource-constrained device has on the order of 1K of RAM, 16K of non-volatile memory (EEPROM or flash) and 24K of ROM. The code for implementing string manipulation, single and double-precision floating point arithmetic, and thread management would be larger than the ROM space on such a device. Even if it could be made to fit, there would be no space left over for class libraries or application code. RAM resources are also very limited. Therefore Java® card technology is implemented as a subset of the Java® platform.
Dynamic class loading is for instance not supported in the Java® card platform. An implementation of the Java® card platform is not able to load classes dynamically. Classes are either masked into the card during manufacturing or downloaded through an installation process after the card has been issued. Programs executing on the card may only refer to classes that already exist on the card, since there is no way to download classes during the normal execution of application code.
Security management in the Java® card platform differs significantly from that of the Java® platform. In the Java® platform, there is a Security Manager class (java.lang.Security Manager) responsible for implementing security features. In the Java® card platform, language security policies are implemented by the virtual machine. There is no Security Manager class that makes policy decisions on whether to allow operations.
In order to check at runtime that the Java® code has been successfully language verified, typically cryptographic methods are employed. This means that the actual deployer, after having performed a Java® language verification, signs the Java® code, i.e., the Java® card CAP file, in such a way that this cryptographic signature can be undeniably cryptographically verified within the embedded microcontroller system, i.e., a Java® virtual machine, that executes the Java® code. This way, the embedded microcontroller system does not need to do within its chip the complete Java® language verification, which, depending on the hardware capabilities of the embedded microcontroller, would either be a prohibitively expensive or a plainly intractable operation. Therefore, the deployer of the preprocessed Java® code establishes the trust in this Java® code by means of a Java® language verification before he signs the resultant file prior to loading it into the embedded microcontroller system.
The problem faced by the deployers of the preprocessed Java® code, e.g., Java® card CAP files, is that they no longer have access to the original Java® class files to be able to verify those themselves. As it is often, for example for copyright or IP reasons, also not an option to freely provide the Java® class files to the deployers of the Java® card CAP files, another solution for establishing the trust in the code contained in a Java® card CAP file needs to be found. One approach would be to develop a complete verifier operating on preprocessed code, e.g., on Java® card CAP files. However, this is a very labor-intensive approach not leveraging the maturity and experiences gained with PC-level Java® class verifiers.